i:Id, ds:x:Id fp Type, da:k:Knd fp Type, x:Id, T:Type, ks:Knd List,
tr:(k:{k:Knd| (k  ks) }State(ds)Valtype(da;k)TT).
ds || x : T  R-state-var(i;ds;da;x;T;ks;tr)  Realizer 

latex

Definitions

t  T, x:A. B(x), Void, x:A. B(x), Top, IdDeq, Id, Type, x.A(x), x. t(x), x : v, P  Q, f(x)?z, f  g, <a,b>, s = t, x:AB(x), P  Q, x:AB(x), P & Q, P  Q, DeclaredType(ds;x), f(a), State(ds), Knd, (x  l), Valtype(da;k), {x:A| B(x) }, @loc effect knd(v:T)  x := f State(ds) v , xL.R(x), @loc only events in L change x:T, left  right, R-state-var(i;ds;da;x;T;ks;tr), a:A fp B(a), type List, f || g, Realizer

Lemmas

fpf-compatible wf, fpf wf, Rplus wf, Rframe wf, Rall wf, Reffect wf, ma-valtype wf, decl-state wf, l member wf, Knd wf, subtype rel dep function, fpf-join wf, fpf-cap wf, fpf-cap-join-subtype, top wf, fpf-compatible-join-cap, fpf-single wf, fpf-cap-single1, Id wf, id-deq wf, subtype rel self